COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\input jmclet
C00004 ENDMK
C⊗;
\input jmclet
\jmclet
\address
Mr. Robert Martin
UNISYS
2400 Colorado Avenue
MS 41-16
Santa Monica, CA  90406
\body

Dear Mr. Martin:

	Dr. Shankar has worked in the Formal Reasoning Group
on a two year appointment as Research Associate since he
received his PhD at the University of Texas in 1986.

	In my opinion his thesis work on making the Boyer-Moore
theorem prover accept a proof of the Goedel incompleteness
theorem and his previous computer assisted proof of the
Church-Rosser theorem constitute the most ambitious and
successful computer-checked mathematical proof that has
been done.  It still hasn't been equalled.

	While at Stanford he has worked on an improved
logic of computer programs and developed ideas of improved
interactive theorem provers.  In both of these areas he
has promising results.

\closing
Sincerely,
John McCarthy
Professor
\endletter
\end